k:Knd, T:Type, l:IdLnk, ds, dt:tg:Id fp Type,
g:(tg:Id(State(ds)T(DeclaredType(dt;tg) List))) List.
(isrcv(k)  destination(lnk(k)) = source(l)  Id & (lnk(k) = l  T = DeclaredType(dt;tag(k))))
 Normal(ds)
 Normal(T)
 Normal(dt)
 sends k(v:T) on l:tagged(g,State(ds),v):dt ||- es.sends k(v:T) on l:tagged(g,State(ds),v):dt 

latex

Definitions

es realizer ind Rsends compseq tag def, Consistent(R;es), P  Q, P & Q, DeclaredType(ds;x), b, Normal(T), Normal(ds), sends k(v:T) on l:tagged(g,State(ds),v):dt, Id, Type, tag(k), Void, f(x)?z, <a,b>, s = t, x:AB(x), ES, t  T, x:A. B(x), sends knd(v:T) on l:tagged(g,State(ds),v):dt, left+right, Knd, x:AB(x), IdLnk, a:A fp B(a), type List, xdom(f). v=f(x)   P(x;v), es realizer ind, isrcv(k), if b t else f fi, source(l), destination(l), Case b of inl(x)  s(x) ; inr(y)  t(y), lnk(k), a = b, A & B, R-Feasible(R), inr(x), R ||- es.P(es), x. t(x), State(ds), Prop

Lemmas

normal-type wf, normal-ds wf, ldst wf, lsrc wf, tagof wf, decl-state wf, decl-type wf, fpf wf, Id wf, IdLnk wf, Knd wf, eq lnk wf, lnk wf, assert wf, isrcv wf, R-consistent wf, Rsends wf, event system wf